As we're trying to program a sorting routine, it would be nice to
be able to define orderings on things, and to do this we need some
representation of boolean variables. Unfortunately TEX doesn't have a type
for booleans, so we'll have to invent our own. We'll
implement a boolean as a function b of the form
#math99#
| b~x~y |
= |
#tex2html_wrap_indisplay2178##tex2html_wrap_indisplay2179# |
|
More formally, a
boolean b is a function which respects equality,
such that for all f, g and z:
and for all f and g which respect equality,
#math101#
| b~(f~b)~(g~b) |
= |
b~(f~First)~(g~Second ) |
|
All the functions in this section satisfy these properties. Surprisingly
enough, so does Error, which is quite useful, as it allows us to
reason about booleans which ``go wrong''.